This application relates to methods for program verification through symbolic enumeration of control path programs.
Symbolic execution has been proposed as a method for generalizing dynamic testing. Initial work focused on generating test sets with better basic block coverage, not necessarily proving satisfiability of program assertions. Recently, work has been done towards using a symbolic execution engine in the refinement step of a predicate abstraction-based model checker. Conventional symbolic execution-based tools employ a combination of concrete and symbolic execution to systematically explore the paths of a given program. The symbolic execution of a given program path computes a set of constraints whose solutions provide inputs for executions along the path. Such inputs yield useful test cases for the program in order to discover potential bugs and to maximize code coverage. The unsatisfiability of the constraints computed along a path indicates the (semantic) unfeasibility of the chosen path. Symbolic execution approaches have been shown to be effective for test generation in order to cover large portions of the program and discover useful bugs in the process. However, the path explosion problem, wherein the large number of program paths to be explored results in numerous expensive satisfiability checks, frequently limits its applicability in practice. A significant fraction of the paths that contribute to the path explosion problem tends to be infeasible. Such paths do not contribute to the overall coverage goals, or lead to useful bugs. Therefore, they are mostly ignored by existing approaches. Secondly, techniques based on symbolic execution expose potential bugs in the programs but not necessarily indicate the absence of such bugs due to the incompleteness of the symbolic execution.
Path programs are syntactic paths in the MSCC graph between the start node and a given property node. They represent a set of syntactic paths through the original program, traversing the same subset of edges but varying in the number of iterations of loops/recurrences encountered in the path. Existing program analysis techniques are mostly path insensitive. This makes the results of the analysis imprecise, leading to problems such as false alarms. Path insensitivity is an important reason for failure to prove properties by static analysis techniques. A completely path sensitive analysis, however, does not scale. Many approaches have been proposed for path sensitive program analysis, including ESP, trace partitioning, elaborations, and others based on disjunctive completion. Significantly, the approaches detailed above allow partial path-sensitivity on top of an underlying framework for path-insensitive analysis. However, conventional approaches typically use heuristics to control the trade-off between performing a join operation as opposed to a logical disjunction at the merge points in the control flow graph. The performance of such heuristics can be highly variable depending on the type of the program being analyzed.